T:Type, Q:((T List)Prop).
Q(nil)  (ys:T List, x:T. Q(ys)  Q(ys @ [x]))  {zs:T List. Q(zs)} 

latex

Definitions	{T}, t  T, Prop, x(s), x:A. B(x), as @ bs, P  Q, ||as||, , ij, False, A, AB, True, T, P & Q, P  Q, x:A. B(x), t  ...$L
Lemmas	length nil, length cons, length append, list decomp reverse, non neg length, length wf1, length zero, le wf, ge wf, nat properties, nat wf, append wf